COMMENT ⊗   VALID 00002 PAGES
C REC  PAGE   DESCRIPTION
C00001 00001
C00002 00002	Supernatural deduction and contexts
C00006 ENDMK
C⊗;
Supernatural deduction and contexts

Features

1. holds (proposition: p, context:c)
   val (term:(v,c)

2. c1≤c2
   c1 is a specialization of c2

3. downward inheritance
   
   holds(p,c2) 1 c1≤c2 ⊃ holds(p,c1)

Remark: Contexts may be indefinite
        w/r proposition, i.e. we can have
        ¬holds(p,c) ∧ ¬holds(¬p,c).

4.  Non-monotonic upwards inheritance
    ¬ab aspect1(p,c1,c2) ∧ holds(p,c1) ⊃ holds(p,c1) ⊃ holds(p,c2)
    ¬ab aspect1(v,c1,c2) ⊃ val(v,c1) = val(v,c2)

A term need not have a value in a context, so we'd better use a relation 
    hasval(v,c,α), but this suggests using merely
    holds(v=α,c)

5. There are a number of specific specifications.

   a. specify(speaker=jmc,e) ≤ c gives a value to I.

   b. specify(time=1986 Mar 21, 2000,c) gives a meaning to now or possibly to
      then.

   c. specify(story=``Sherlock Holmes,c1) has a meaning only in those contexts
      in which ``the Shelock Holmes stories'' is meaningful.

6. Trade-off relations between specificity of contests and specificity of sentences

   holds(at(jmc,Asilomar),specify(date=1986,Mar21,c)
   ≡holds(on-date(1986Mar21,at(jmc,Asilomar)),c)

7. Supernatural deduction. The phrase means that I hope to be able to claim that
   it is more natural than traditional natural deduction.

   When we have holds(p,c), we may declare

   enter c:

   and write

   p.

   If we then reason within statements that hold within c and deduce 

   q,

   we can then discharge c and write 

   holds(q,c)

   In the deduction we can always write a sentence r if we have holds(r,c')
   and c≤c'

8. We hope to allow contexts within contexts, e.g.

   holds(holds(p,c1),c2)

   Here are some applications. We can put sentences with contexts in our common
   sense database. We can then expand to wider contexts using non-monotonic
   upwards inheritance getting {\it elaboration tolerance\/} and {\it ambiguity
   tolerance\/}.